;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
; The Hipstafy module's interface, which is the module
; responsible for creating the Andy Warhol-esque images
(interface IHipstafy
  
  (sig hipstafy (tree))
  (sig hipstafy-helper (width height oldtree newtree xcurr xmax ycurr ymax))
  
  ; verifies that the hipstafy function returns a tree
  (con hipstafy-returns-tree
       (implies (tree? tr))
       (tree? (hipstafy tr)))
  
  ; verifies that the hipstafy-helper function returns a tree
  ; (width height oldtree newtree xcurr xmax ycurr ymax)
  (con hipstafy-helper-returns-tree
       (implies (natp width) (natp height) (tree? oldtr) (tree? newtr)
                (= xcurr 0) (= ycurr 0) (natp xmax) (natp ymax))
       (tree? (hipstafy-helper width height oldtr newtr xcurr xmax ycurr ymax))))